#define NB_CLAUSES 320

/**
 * get the warp number of this instance
 */
__device__ int warpnb(){
	return threadIdx.x/32;
}

/**
 * returns the formula number(of the initial batch)
 */
__device__ unsigned int nbformule(int warp){
	return blockIdx.x*2 + warp/3;
}

/**
 * return the affectation corresponding to formula nbformule and warp nwarp
 * 
 */
__device__ unsigned int getaffectation(unsigned int nbformule, int nwarp, unsigned int *tab){
	unsigned int valeur = tab[nbformule*NB_CLAUSES];
	char affected = (valeur >> 24);
	int sum = affected %4;
	if(sum <= nwarp){
		return ((unsigned int)1)<<31;
	}
	switch(nwarp){
		case 0:
			{return (valeur^128) %256 + (1<<24);}
		
		case 1:
			{
				return ((valeur)^(1<<15)) % (1<<16) + (2 <<24);}
		
		case 2:
			{return (valeur % (1<<24))^(1<<23) +(3 <<24);}
		
		default:
			return 0;
	}
}

/**
 * set a flag on invalid to declare the formula a as invalid
 */
__device__ void setInvalidFormula(int a, int* invalid){
	invalid[a]=0;
}

/**
 * set a flag in goodclauses to declare the clause index as verified
 */
__device__ void setVerifiedClause(int index, int* goodclauses){
	goodclauses[index]=0;
}

/**
 * compute the clause resulting after the affectation affect and store it in tabsortie
 */
__device__ void affectclause(int clausenb, int nbformule, unsigned int affect, unsigned int *tab, unsigned int *tabsortie,int k,int* invalidformula, int* verifiedclauses){
	unsigned int clause = tab[nbformule*NB_CLAUSES + clausenb];
	if((clause>>31)==1){
		tabsortie[k]=clause;
		setVerifiedClause(k,verifiedclauses);
		return;
	}
	
	char nbaffectation = (affect>>24) % 8;
	char nbliteraux = (clause>>24) % 8;
	unsigned int sortie = 0;
	unsigned int index = 0;
	int l=0,c=0;
	bool changed = false;
	if(nbliteraux!=0){
		// for each literal
		for(l=0; l< nbliteraux; l++){
			changed = false;
			for(c=0; c<nbaffectation; c++){
				if(((clause >> (8*l)) %128) == ((affect >> (8*c)) %128)){
					// if the variable is used in this clause
					changed = true;// we can replace it with its value
					if(((clause>>(8*l))%256) != ((affect>>(8*c))%256)){
						// 
						sortie |= (((unsigned int)1)<<31);
						setVerifiedClause(k, verifiedclauses);//the clause is nullified
						tabsortie[k]=0;
						return;
					}
				}
			}
			if(!changed){
				// we don't know the value, we put it in the output clause
				sortie += ((unsigned int) ((clause >> (8*l)) % 256))<<(8*index);
				index++;
			}
		}
		if(index==0){
			// all literals are know but none of them verifies the formula
			setInvalidFormula(k/NB_CLAUSES, invalidformula);
		}
	}
	else{
		// no literals remaining, the clause is verified !
		sortie =0;
		setVerifiedClause(k, verifiedclauses);
	}
	tabsortie[k] = sortie+(((unsigned int)index)<<24);
}

/**
 * apply the sat rules on the formulas in tab limiting withe batchsize
 */
__global__ void applyrules(int n, unsigned int *tab, unsigned int *tabtmp, int* invalidformula, int* verifiedclauses, int batchsize){
	__shared__ unsigned int affectation[6];
	int thid = threadIdx.x;
	int nbwarp = warpnb();
	unsigned int formulenb = nbformule(nbwarp);
	if(thid<6){
		//affectation = (unsigned int*) malloc(6*sizeof(unsigned int));
		affectation[thid] = getaffectation(formulenb+thid/3, thid%3, tab);
	}
	__syncthreads();
	if(formulenb<batchsize){
		if(affectation[nbwarp] != (((unsigned int)1)<<31)){ 
			int i=0;
			for(i=threadIdx.x % 32; i<NB_CLAUSES; i += 32){
				affectclause(i, formulenb, affectation[nbwarp], tab, tabtmp, (formulenb*3+(nbwarp%3))*NB_CLAUSES+i, invalidformula, verifiedclauses);
			}
		}
		else{
			setInvalidFormula((formulenb*3+(nbwarp%3)),invalidformula);
		}
	}
}
